es:ES, i, x, y:Id, I:(vartype(i;x)vartype(i;y)Prop).
e@i. first(e)  I(x when e,y when e) & e@i. I(x when e,y when e)  I((x after e),(y after e))
 @i always.I(x,y) 

latex

Definitions	vartype(i;x), loc(e), (x after e), pred(e), x when e, @i always.P(x1;x2), x. t(x), e@i. P(e), E, A, b, first(e), Prop, P  Q, P & Q, P  Q, P  Q, x(s1,s2), ES, Id, x:A. B(x), T, True, t  T
Lemmas	es-vartype wf, es-when wf, es-after-pred, es-loc-pred, es-after wf, es-pred wf, es-loc wf, es-first wf, assert wf, not wf, alle-at-iff, true wf, squash wf, event system wf, Id wf, alle-at wf, es-E wf